(declare-fun i1 () Int)
(declare-fun i5 () Int)
(declare-fun i7 () Int)
(declare-fun ufbi7 (Bool Bool Bool Bool Bool Bool Bool) Int)
(declare-fun ufii3_2 (Int Int Int) Int)
(declare-fun ufii6_2 (Int Int Int Int Int Int) Int)
(declare-fun v3 () Bool)
(declare-fun v4 () Bool)
(declare-fun i8 () Int)
(declare-fun i9 () Int)
(declare-fun v5 () Bool)
(declare-fun v6 () Bool)
(declare-fun v8 () Bool)
(declare-fun v9 () Bool)
(declare-fun v10 () Bool)
(declare-fun i13 () Int)
(declare-fun v19 () Bool)
(declare-fun i14 () Int)
(assert (and (= (and v3 v8) (= i8 i9)) (or v4 (= 1 i9))))
(assert (distinct 0 1 i8 i7))
(assert (or v9 (= 1 (mod (ufbi7 v3 (and (> i13 2) (> (abs i14) i13) (> (ufii3_2 (* i5 2) 1 i7) (abs i14)) (> (+ i7 2 2 i1) (ufii3_2 (* i5 2) 1 i7))) (and (not v6) (not v10) (< 1 (* 2 i5 i5))) (and (>= 4 i7) (>= i7 i5) (>= i5 (abs (+ i7 2 2))) (>= (div (* i1 2) 4) 0) (>= (abs (+ i7 2 2)) (div (* i1 2) 4))) (distinct i9 (div (* i1 2) 4) 2 i8 (* i5 2)) v19 false) 4))))
(assert (or v8 (and (= i5 1) (= i9 (abs i8)))))
(assert (or v5 (= 0 (ufii6_2 1 1 0 1 (* i9 i9) (mod (ufbi7 false (and (> i13 2) (> (abs i14) i13) (> (ufii3_2 (* i5 2) 1 i7) (abs i14)) (> (+ i7 2 2 i1) (ufii3_2 (* i5 2) 1 i7))) (and (= v6 false) (= v10 false) (< 1 (* i5 2 i5))) (and (>= 4 i7) (>= i7 i5) (>= i5 (abs (+ i7 2 2))) (>= (div (* i1 2) 4) 0) (>= (abs (+ i7 2 2)) (div (* i1 2) 4))) (distinct i9 (div (* i1 2) 4) 2 i8 (* i5 2)) v19 false) 4)))))
(assert (or (= i9 0) (= 1 i14)))
(check-sat)
